| Definitions | t  T, IdDeq, x:A  B(x),  b, ES, Type, a:A fp B(a),  e@i. P(e), Atom$n, Id, if b then t else f fi , x:A B(x), P   Q, x:A. B(x), P & Q, P  Q, MaInterface(T), ma-interface-locs(I), Top, type List, (x l), {x:A| B(x)} , x dom(f), ma-interface-consistent-at(es;i;X), ma-interface-consistent(es;X), ma-interface-consistent2(es;I), s = t, Knd, State(ds), left + right, f(x), strong-subtype(A;B),   x. t(x), EqDecider(T), KindDeq,  ,  , valtype(e), t.1, vartype(i;x), f(x)?z, ma-interface-dom(I;i), a < b, hasloc(k;i), x.A(x), fpf-domain(f), A c B,  ,  x:A. B(x), <a, b>, True,  T, Unit, tt, ff,   b, IdLnk, case b of inl(x) => s(x) | inr(y) => t(y), S  T, Void,  x:A.B(x), t.2, s ~ t, {T}, SQType(T), E, ma-interface-valtype(I;i;k), P Q, let x,y = A in B(x;y), f(a), ma-interface-info(I;i;k), ma-interface-ds(I;i), x(s) |